NOTE : OUR COMMENTS WERE MARKED IN BRACKETS [ ... ].
COMMENTS MARKED WITH THE ADJECTIVE "OBVIOUS" REFER
TO FACTUALLY WRONG STATEMENTS CONTRADICTING
COMMON COMPUTER SCIENCE KNOWLEDGE OR FORMAL
PROPERTIES OF THE PAPER
 (LIKE "HAS NO EXPERIMENTAL EVALUATION" ETC.).
WE DO NOT CRITICISE NECESSARILY SUBJECTIVE
STATEMENTS ON SIGNIFICANCE, RELEVANCE OR
ORIGINALITY, JUST TECHNICAL ACCURACY.

COUNT ON OBVIOUS FACTUAL INACCURACIES: 7.

---------------------------------------------

Paper: 1
Title: Firewall Testing Reloaded: A New Technique in Policy Testing

-------------------- review 1 --------------------

PAPER: 1
TITLE: Firewall Testing Reloaded: A New Technique in Policy Testing

OVERALL RATING: -2 (reject) 
REVIEWER'S CONFIDENCE: 3 (high)  
----------------------- REVIEW --------------------

The authors present in this contribution an extension of their firewall testing approach presented at last year TestCom. They presented a method using semantics-preserving transformation rules which allows to reduce the complexity of the firewall rules and thus the number of test cases needed. As the authors state the did not apply their approach to practice so far so that it is a theoretical approach up to now. Therefore also the improvement by the described approach becomes not really visible. It is also not clear said how the test should be applied. Security officers often add, remove or change rules. How the approach supports such incremental changes?

The described model confines to simple packet filtering rules to block or pass packets of a certain protocol. How it applies to more complex firewall rules? The modeling(or the wording)applied, however,seem strange. The packet model introduced in 3.1 is related to the transport layer,

[That is correct. It is exactly on the layer, in which rules are specified in all firewall configuration tools I am aware of. See our paper in 2008 (The Section explicit REVISITS
this model, consequently we can't give any motivation.)].

but it should be the IP layer, since only IP addresses and the protocol number are considered which are not part of the transport layer. The refined address model at the end of 3.1

[That is not the case. Following your argument, one would *have* to test any program on the assembler level --- contraryly what MODEL-BASED Tests is standing for.
 Our tests correspond exactly to the level of abstraction  in which you configure a firewall.]

corresponds to the transport layer, since it takes the ports into account. It is further not clear, why the authors introduce network address translation. The rule (8) is too general to express the essence of NAT. In addition, NAT is not a firewall rule in the closer sense. It is not needed here.  

The paper is too long and tediously written. 

[It is 16 2/3 pages long and roughly in the space limit. The appendix with the formal proof is just for the referees. ]

The inner logic of the paper disappears under a broad and tedious representation. 

[Problematically subjective: You mean - it contains definitions and a formal proof ? ]

Some of the rules and examples should be more commented, e.g. (10), (11), (16) (why "some deny" ?),(17). An application to real firewall rules should be applied to demonstrate the need and the usefulness of the proposed approach. 

[Obviously wrong: We gave a 2 page description of experimental results of the ETH Zürich network. 
 We do not know about any tool that can do better.]

-------------------- review 2 --------------------

PAPER: 1
TITLE: Firewall Testing Reloaded: A New Technique in Policy Testing

OVERALL RATING: 0 (borderline paper) 
REVIEWER'S CONFIDENCE: 3 (high)  
----------------------- REVIEW --------------------

The authors describe an optimization technique for model-based generation
of test-cases for firewalls. It is an interesting and formal approach.
However, the reviewer has the following reservations:

(1) The main contribution is on formality and transformation but 
there is very little on "optimization". The claim of

[Obviously factually wrong: The pages 7-13 are completely devoted to optimization.
 We can not see the point that presenting an optimization rule formally diminishes
 its value of beeing an optimization. DenyAll ++ DenyAll ++ X = DenyAll ++ X
simplifiies the case distinction structure, and is fully formal.]

"The resulting procedure is characterized by a gain in efficiency of two
orders of magnitude and can handle configurations with hundreds of rules
as occur in practice." 
is not well substantiated.

[Factually wrong: We wrote 2 pages with experimental results which just show
 that. Or are you criticizing that we should have written "up to 2 orders of magnitude?"]

(2)"The correctness of the rules and the algorithm is established
by formal proofs in Isabelle/HOL."
My understanding of Isabelle/HOL is that it is a validation tool and 
not a real "proof". 

[This is obvious factual nonsense. Use wikipedia or google Isabelle/HOL. By the way, it is our main
contribution to have a REAL FORMAL PROOF for our correctness theorem.
In case that you did not notice: it is shown for the referees in the Appendix.]

(3) "Our approach can be seen as an instance of a methodology to tame inherent
state-space explosions in test-case generation for security policies."
This work really has nothing to do with state-space explosion in test generation
for security policies.

[Obviously highly unlikely. If you really believe that we found a way around the state space
explosion problem in model exploration techniques, you should have given us
the Turing award: this would turn P=NP into a corrollary. 
We wrote in sec 2.2. that HOL-TestGen is based on a case splitting technique
of the free or quantified variables... Together with the if-then-elses used for the
override operators, In the concrete model, this blows up the
proof state exponentially ... ]

(4) The firewall policies in real systems are much more complex than what is described here. 

[Obviously wrong. Actually, we mentioned explicitly here that
we analysed a part of the policy of the network of the ETH Zürich.]

-------------------- review 3 --------------------

PAPER: 1
TITLE: Firewall Testing Reloaded: A New Technique in Policy Testing

OVERALL RATING: 0 (borderline paper) 
REVIEWER'S CONFIDENCE: 2 (medium)  
----------------------- REVIEW --------------------

Although this seems to be an interesting piece of work, 
the paper itself is hard to read for a newbie for HOL. 
The paper should extend a little the explaination of the concepts
and syntax of HOL.
The most critics however is that the test case generation is not 
explained.

[Obviously problematic argument: Following this criticism, no application paper using, say, SPIN, should
ever be written without explaining how it works. I qoute from our paper:
"HOL-TestGen is an interactive, i. e. semi-automated, test tool for speciﬁcation- 
based tests built upon Isabelle/HOL. Its theory and implementation has been 
described elsewhere [3–5]; here, we brieﬂy review main concepts ..."]

Does it generate a test case for any potential value of
the firewall policies. 

 [ Obviously: See the shown test specification: "FUT x = ... ". x is of course any input.] 

[Obviously: See the shown test specification  FUT x = ...
x is "any input."]

Or, are representative values (after e.g.
an equivalence partition) taken only? What at all is the understanding
of a testcase in this paper? 

[Again: has been described elsewhere [3–5]; ]

Does it check for the pass-through traffic
only or also for the traffic to be blocked? Do the test cases involve
parallel traffic flows or just single flows? I believe that the
test cases and their properties deserve a section in themselves.
Some further points:
The equivalence for the small example given on page 3 hold only for 
natural/integer-valued x. This should be noted explicitly.
Shouldn't the firewall policy on page 5 in (7) defined to be 
"alpha accept | alpha deny"?!

[Well, I agree that we assume familiarity with elementary  functional programming notation - 
maybe we will have to find a way around this. As in OCaml, SML or Haskell, the notation
"accept \alpha | deny" for a datatype means that there are two constructors, one accept, one deny,
while the former has one argument (of arbitrary type, representing that the format of the 
IP packages is actually irrelevant for this part of the theory.) ]

Please correct the typo "based its address and port" --> 
"based on its address and port"
Please explain also the meaning of "Some(deny)" in (10).
Is "Some deny" in (16) same as "Some(deny)" in (10)? 

[In alll listed functional programming languages, this is actually equivalent.]